Lambda the Ultimate

Paul McJones alerts us that the ACM posted PDF versions of some books in its Classic Books Series, which are available to anyone who creates a free ACM Web Account.

Among the currently available books, LtU readers are likely to be particularly interested in Hoare and Jones's Essays in computing science, Adele Goldberg and David Robson's Smalltalk-80: the language and its implementation, and Dahl, Dijkstra, and Hoare's Structured programming.

Long time readers will also know that I highly recommend Papert's Mindstorms: children, computers, and powerful ideas to anyone interested with the effect computers might have on education. Papert's Logo remains to this day the best children oriented programming language, but even if you disagree with me about this, his book is a must read.

Aydemir, Charguéraud, Pierce, Pollack, and Weirich. Engineering Formal Metatheory.

Machine-checked proofs of properties of programming languages have become a critical need, both for increased confidence in large and complex designs and as a foundation for technologies such as proof-carrying code. However, constructing these proofs remains a black art, involving many choices in the formulation of definitions and theorems that make a huge cumulative difference in the difficulty of carrying out large formal developments. The representation and manipulation of terms with variable binding is a key issue.

We propose a novel style for formalizing metatheory, combining locally nameless representation of terms and cofinite quantification of free variable names in inductive definitions of relations on terms (typing, reduction, . . . ).

...

We have carried out several large developments in this style using the Coq proof assistant and have made them publicly available. Our developments include type soundness for System F_<: and core ML (with references, exceptions, datatypes, recursion, and patterns) and subject reduction for the Calculus of Constructions.

A fairly recent paper from the POPLmark team, which describes an approach to formalizing programming metatheory that they think performs well on the POPLmark challenge criteria (low formalization overhead, low cost of entry, and reasonable similarity to existing informal proof techniques). It looks like this is related to some of the material presented in the How to write your next POPL paper in Coq tutorial at POPL'08, which was previously mentioned on LtU.

So, what are your prediction for 2008? Naturally, we are only interested with predictions related to programming languages...

Three types of predictions are thus in order: (1) Predictions about PLT research (direction, fads, major results) (2) Predictions about programming languages (whether about specific languages, or about families etc.) and (3) Predictions about industrial use of languages/language-inspired techniques (adoption, popularity).

From Arxiv:

A fully-automated algorithm is developed able to show that evaluation of a given untyped lambda-expression will terminate under CBV (call-by-value). The ``size-change principle'' from first-order programs is extended to arbitrary untyped lambda-expressions in two steps. The first step suffices to show CBV termination of a single, stand-alone lambda-expression. The second suffices to show CBV termination of any member of a regular set of lambda-expressions, defined by a tree grammar. (A simple example is a minimum function, when applied to arbitrary Church numerals.) The algorithm is sound and proven so in this paper. The Halting Problem's undecidability implies that any sound algorithm is necessarily incomplete: some lambda-expressions may in fact terminate under CBV evaluation, but not be recognised as terminating.
The intensional power of the termination algorithm is reasonably high. It certifies as terminating many interesting and useful general recursive algorithms including programs with mutual recursion and parameter exchanges, and Colson's ``minimum'' algorithm. Further, our type-free approach allows use of the Y combinator, and so can identify as terminating a substantial subset of PCF.

To renew the discussion on Total Functional Programming, this paper is an alternative to Termination Checking with Types.

A short article by Robert Dewar and Edmond Schonberg. The authors claim that Computer Science (CS) education is neglecting basic skills, in particular in the areas of programming and formal methods. We consider that the general adoption of Java as a first programming language is in part responsible for this decline, but also explain why - in their opinion - C, C++, Lisp, Ada and even Java are all crucial for the education of software engineers.

We identify the following requirements for general extension and composition of software systems:

1. Orthogonal extension: Extensions may require both new data types and new operations.
2. Type safety: Extensions cannot create run-time type errors.
3. Modularity: The base system can be extended without modifying or recompiling its code.
4. Scalability: Extensions should be scalable. The amount of code needed should be proportional to the functionality added.
5. Non-destructive extension: The base system should still be available for use within the extended system.
6. Composability of extensions.

The first three of these requirements correspond to Wadler’s expression problem. Scalability (4) is often but not necessarily satisfied by supporting separate compilation; it is important for extending large software. Non-destructive extension (5) enables existing clients of the base system and also the extended system itself to interoperate with code and data of the base system, an important requirement for backward compatibility. Nested inheritance addresses the first five requirements, but it does not support extension composition. Nested intersection adds this capability.

Multiple dispatch – the selection of a function to be invoked based on the dynamic type of two or more arguments – is a solution to several classical problems in object-oriented programming. Open multi-methods generalize multiple dispatch towards open-class extensions, which improve separation of concerns and provisions for retroactive design. We present the rationale, design, implementation, and performance of a language feature, called open multi-methods, for C++ . Our open multi-methods support both repeated and virtual inheritance... ...our approach is simpler to use, catches more user mistakes, and resolves more ambiguities through link-time analysis, runs significantly faster, and requires less memory. In particular, the runtime cost of calling an open multimethod is constant and less than the cost of a double dispatch (two virtual function calls). Finally, we provide a sketch of a design for open multi-methods in the presence of dynamic loading and linking of libraries.

Who said C++ isn't evolving?

The discussion in section 4 of the actual implementation (using EDG) is particularly detailed, which is a bonus.

The worker/wrapper transformation is a technique for changing the type of a computation, usually with the aim of improving its performance. It has been used by compiler writers for many years, but the technique is little-known in the wider functional programming community, and has never been formalised. In this article we explain, formalise, and explore the generality of the worker/wrapper transformation. We also provide a systematic recipe for its use, and illustrate the power of this recipe using a range of examples.

While the basic idea behind the worker/wrapper transformation should be trivial to any programmer, this paper shows the added value that comes from formal analysis and the usefulness of the algebraic approach.

The paper may be slightly too long for those used to reading work of this type, but since all the examples are presented in detail it should be more accessible to newcomers than many other similar papers.

Lemonodor has the story, and the links, starting with Dan Weinreb's blog post. Yes, Dan Weinreb has a blog, so if you weren't paying attention, now is the time to check it out!

For me, the take home message is from Paul Graham: If the Lisp machines were so gratuitously, baroquely complex, I should really find the time to learn more about them...

Happy new year, everyone!

We describe several views of the semantics of a simple programming language as formal documents in the calculus of inductive constructions that can be verified by the Coq proof system. Covered aspects are natural semantics, denotational semantics, axiomatic semantics, and abstract interpretation. Descriptions as recursive functions are also provided whenever suitable, thus yielding a a verification condition generator and a static analyser that can be run inside the theorem prover for use in reflective proofs. Extraction of an interpreter from the denotational semantics is also described. All different aspects are formally proved sound with respect to the natural semantics specification.

More work on mechanized metatheory with an eye towards naturalness of representation and automation. This seems to me to relate to Adam Chlipala's work on A Certified Type-Preserving Compiler from Lambda Calculus to Assembly Language, which relies on denotational semantics and proof by reflection, in crucial ways. More generally, it seems to reinforce an important trend in using type-theory-based theorem provers to tackle programming language design from the semantic point of view (see also A Very Modal Model of a Modern, Major, General Type System and Verifying Semantic Type Soundness of a Simple Compiler). I find the trend exciting, but of course I also wonder how far we can practically go with it today, given that the overwhelming majority of the literature, including our beloved Types and Programming Languages, is based on A Syntactic Approach to Type Soundness. Even the upcoming How to write your next POPL paper in Coq at POPL '08 centers on the syntactic approach.

Is the syntactic approach barking up the wrong tree, in the long term? The semantic approach? Both? Neither?